\begin{tabbing}
$\forall$${\it ds}$:fpf(Id; $x$.Type), ${\it da}$:fpf(Knd; $k$.Type), $A$,$B$:ecl{-}trans{-}tuple\=\{i:l\}\+
\\[0ex](${\it ds}$; ${\it da}$).
\-\\[0ex]ecl{-}trans{-}normal($A$)
\\[0ex]$\Rightarrow$ ecl{-}trans{-}normal($B$)
\\[0ex]$\Rightarrow$ \=($\forall$$n$:$\mathbb{N}$, ${\it L'}$:(event{-}info(${\it ds}$;${\it da}$) List).\+
\\[0ex](ecl{-}trans{-}halt2(${\it ds}$; ${\it da}$; $A$)($n$,${\it L'}$))
\\[0ex]$\Rightarrow$ \=($\forall$$L$:(event{-}info(${\it ds}$;${\it da}$) List). \+
\\[0ex]iseg(event{-}info(${\it ds}$;${\it da}$); ${\it L'}$; $L$) $\Rightarrow$ (ecl{-}trans{-}halt2(${\it ds}$; ${\it da}$; $A$)($n$,$L$))))
\-\-\\[0ex]$\Rightarrow$ \=($\forall$$n$:$\mathbb{N}$, ${\it L'}$:(event{-}info(${\it ds}$;${\it da}$) List).\+
\\[0ex](ecl{-}trans{-}halt2(${\it ds}$; ${\it da}$; $B$)($n$,${\it L'}$))
\\[0ex]$\Rightarrow$ \=($\forall$$L$:(event{-}info(${\it ds}$;${\it da}$) List). \+
\\[0ex]iseg(event{-}info(${\it ds}$;${\it da}$); ${\it L'}$; $L$) $\Rightarrow$ (ecl{-}trans{-}halt2(${\it ds}$; ${\it da}$; $B$)($n$,$L$))))
\-\-\\[0ex]$\Rightarrow$ \=($\forall$$n$:$\mathbb{N}^{+}$, $L$:(event{-}info(${\it ds}$;${\it da}$) List).\+
\\[0ex](ecl{-}trans{-}halt2(${\it ds}$; ${\it da}$; $A$)($n$,$L$)) $\Rightarrow$ ($n$ $\in$ ecl{-}trans{-}es($A$)))
\-\\[0ex]$\Rightarrow$ \=($\forall$$n$:$\mathbb{N}^{+}$, $L$:(event{-}info(${\it ds}$;${\it da}$) List).\+
\\[0ex](ecl{-}trans{-}halt2(${\it ds}$; ${\it da}$; $B$)($n$,$L$)) $\Rightarrow$ ($n$ $\in$ ecl{-}trans{-}es($B$)))
\-\\[0ex]$\Rightarrow$ \=($\forall$$f$:((?$\mathbb{B}$)$\rightarrow$($\mathbb{N}\rightarrow\mathbb{B}$)$\rightarrow$($\mathbb{N}\rightarrow\mathbb{B}$)$\rightarrow\mathbb{N}\rightarrow\mathbb{B}$), $g$:($\mathbb{B}\rightarrow\mathbb{B}\rightarrow\mathbb{B}\rightarrow\mathbb{B}\rightarrow\mathbb{B}\rightarrow\mathbb{B}\rightarrow\mathbb{B}$), $L$:(event{-}info(${\it ds}$;${\it da}$) List).\+
\\[0ex]$\exists$\=$x$:?$\mathbb{B}$\+
\\[0ex]((\=ecl{-}trans{-}state(combine{-}ecl{-}tuples2($A$; $B$; $f$; $g$); $L$)\+
\\[0ex]=
\\[0ex]$<$ecl{-}trans{-}state($A$; $L$), ecl{-}trans{-}state($B$; $L$), $x$$>$
\\[0ex]$\in$ ecl{-}trans{-}type(combine{-}ecl{-}tuples2($A$; $B$; $f$; $g$)))
\-\\[0ex]$\wedge$ \=(($x$ = (inl tt ))\+
\\[0ex]$\Leftarrow\!\Rightarrow$ ($\exists$\=${\it L'}$:event{-}info(${\it ds}$;${\it da}$) List\+
\\[0ex]$\exists$\=$m$:$\mathbb{N}$\+
\\[0ex](iseg(event{-}info(${\it ds}$;${\it da}$); ${\it L'}$; $L$)
\\[0ex]$\wedge$ (ecl{-}trans{-}halt2(${\it ds}$; ${\it da}$; $A$)($m$,${\it L'}$))
\\[0ex]$\wedge$ \=($\forall$$n$:$\mathbb{N}$, ${\it L''}$:(event{-}info(${\it ds}$;${\it da}$) List).\+
\\[0ex]iseg(event{-}info(${\it ds}$;${\it da}$); ${\it L''}$; ${\it L'}$)
\\[0ex]$\Rightarrow$ (ecl{-}trans{-}halt2(${\it ds}$; ${\it da}$; $B$)($n$,${\it L''}$))
\\[0ex]$\Rightarrow$ (${\it L''}$ = ${\it L'}$))
\-\\[0ex]$\wedge$ ($\forall$$n$:int\_seg(0; $m$). $\neg$(ecl{-}trans{-}halt2(${\it ds}$; ${\it da}$; $B$)($n$,${\it L'}$))))))
\-\-\-\\[0ex]$\wedge$ \=(($x$ = (inl ff ))\+
\\[0ex]$\Leftarrow\!\Rightarrow$ ($\exists$\=${\it L'}$:event{-}info(${\it ds}$;${\it da}$) List\+
\\[0ex]$\exists$\=$m$:$\mathbb{N}$\+
\\[0ex](iseg(event{-}info(${\it ds}$;${\it da}$); ${\it L'}$; $L$)
\\[0ex]$\wedge$ (ecl{-}trans{-}halt2(${\it ds}$; ${\it da}$; $B$)($m$,${\it L'}$))
\\[0ex]$\wedge$ \=($\forall$$n$:$\mathbb{N}$, ${\it L''}$:(event{-}info(${\it ds}$;${\it da}$) List).\+
\\[0ex]iseg(event{-}info(${\it ds}$;${\it da}$); ${\it L''}$; ${\it L'}$)
\\[0ex]$\Rightarrow$ (ecl{-}trans{-}halt2(${\it ds}$; ${\it da}$; $A$)($n$,${\it L''}$))
\\[0ex]$\Rightarrow$ (${\it L''}$ = ${\it L'}$))
\-\\[0ex]$\wedge$ ($\forall$$n$:int\_seg(0; ($m$ + 1)). $\neg$(ecl{-}trans{-}halt2(${\it ds}$; ${\it da}$; $A$)($n$,${\it L'}$))))))
\-\-\-\\[0ex]$\wedge$ \=(($\neg$($\uparrow$isl($x$)))\+
\\[0ex]$\Leftarrow\!\Rightarrow$ \=($\forall$$m$:$\mathbb{N}$. \+
\\[0ex]($\neg$(ecl{-}trans{-}halt2(${\it ds}$; ${\it da}$; $A$)($m$,$L$))) $\wedge$ ($\neg$(ecl{-}trans{-}halt2(${\it ds}$; ${\it da}$; $B$)($m$,$L$)))))))
\-\-\-\-
\end{tabbing}